\begin{tabbing}
$\forall$${\it es}$:ES, $P$:(E$\rightarrow\mathbb{B}$), $e$:E.
\\[0ex](($\uparrow$($e$ $\in_{b}$ last($P$))) $\Leftarrow\!\Rightarrow$ ($\exists$$a$:E. (($a$ $<$loc $e$) \& ($\uparrow$($P$($a$))))))
\\[0ex]\& (\=($\uparrow$($e$ $\in_{b}$ last($P$)))\+
\\[0ex]$\Rightarrow$ \=((last($P$)($e$) $<$loc $e$)\+
\\[0ex]\& ($\uparrow$($P$(last($P$)($e$))))
\\[0ex]\& ($\forall$${\it e''}$:E. (${\it e''}$ $<$loc $e$) $\Rightarrow$ (last($P$)($e$) $<$loc ${\it e''}$) $\Rightarrow$ ($\neg$($\uparrow$($P$(${\it e''}$)))))))
\-\-
\end{tabbing}